(module subtyping (lib "eopl.ss" "eopl")
  
  (require "lang.scm")
  (require "static-data-structures.scm")
  (require "expand-type.scm")
  (require "renaming.scm")
  (require "substitutions.scm")

  (provide <:-module-type)

  (define <:-module-type
    (lambda (m-type1 m-type2 tenv)
      (let ()
        ;; these are already expanded
        ;; ((m-type1 (expand-module-type-in-tenv m-type1 tenv))
        ;;  (m-type2 (expand-module-type-in-tenv m-type2 tenv)))
        (cases module-type m-type1
          (env-module-type (decls1)
            (cases module-type m-type2
              (env-module-type (decls2)
                (<:-declarations decls1 decls2 tenv))
              (else #f)))
          (proc-module-type (param-name1 param-type1 m-type1)
            (cases module-type m-type2
              (proc-module-type (param-name2 param-type2 m-type2)
                ;; first we rename the param names to the same fresh name
                (let ((new-name (fresh-module-name param-name1)))
                  (let ((m-type1
                          (rename-in-module-type
                            m-type1 param-name1 new-name)) 
                        (m-type2
                          (rename-in-module-type
                            m-type2 param-name2 new-name)))
                    (and
                      (<:-module-type param-type2 param-type1 tenv)
                      (<:-module-type m-type1 m-type2
                        (extend-tenv-with-module
                          new-name param-type2 tenv))))))
              (else #f)))
          ))))

  ;; (trace <:-module-type)


  ;; s1 <: s2 iff s1 has at least as much stuff as s2.  Hence we walk
  ;; down s2 and see if each component has a matching component in
  ;; s1.  For the moment, these have to match in order, so that the
  ;; types have the right scope.  Relaxing this restriction should
  ;; become an exercise.

  (define <:-declarations
    (lambda (decls1 decls2 tenv)
      (cond
        ;; if nothing in decls2, any decls1 will do
        ((null? decls2) #t)
        ;; nothing in decls1 to match, so false
        ((null? decls1) #f)
        (else
          ;; at this point we know both decls1 and decls2 are
          ;; non-empty
          (let ((name1 (decl->name (car decls1)))
                (name2 (decl->name (car decls2))))
            (if (eqv? name1 name2)
              ;; same name.  They'd better match
              (if (<:-declaration (car decls1) (car decls2) tenv)
                (<:-declarations (cdr decls1) (cdr decls2)
                  (extend-tenv-with-declaration
                    (car decls1) tenv))
                #f)
              ;; different names.  OK to skip 
              (<:-declarations (cdr decls1) decls2
                (extend-tenv-with-declaration
                  (car decls1) tenv))))))))

  ;; decl1 and decl2 are known to declare the same name
  (define <:-declaration 
    (lambda (decl1 decl2 tenv)
      (cond
        ((and (val-decl? decl1) (val-decl? decl2))
         (<:-type (decl->type decl1) (decl->type decl2) tenv))
        ((and (abstype-decl? decl1) (abstype-decl? decl2))
         #t)
        ((and (type-abbrev-decl? decl1) (type-abbrev-decl? decl2))
         ;; Leroy's ~~
         (equiv-type? (decl->type decl1) (decl->type decl2) tenv))
        ;; any type-abbrev matches an abstype
        ((and (type-abbrev-decl? decl1) (abstype-decl? decl2))
         #t)
        ;; but not vice versa, or anything else.
        (else #f))))

  ;; (trace <:-declaration)

  ;; <:-type : type * type * tenv -> (maybe subst)

  ;; ty1 may contain type variables.  Since these have already been
  ;; expanded, we know that they are unconstrained.  So we should have

  ;; E |- (t37 -> t37) <: (t -> t)

  ;; if t is bound in E.

  ;; This will be like the unifier, except that ty2 is guaranteed not
  ;; to contain any type variables.

  (define <:-type
    (lambda (ty1 ty2 tenv)
      ;; (eopl:printf "entering <:-type~%")
      ;; start by expanding all the types
      (let recur 
        ((ty1 (expand-type-in-tenv ty1 tenv))
         (ty2 (expand-type-in-tenv ty2 tenv))
         (subst (empty-subst)))
        ;; ((ty1 ty1) (ty2 ty2) (subst (empty-subst)))
        (cond
          ((equal? ty1 ty2) subst)            
          ((tvar-type? ty1)
           ;; since we've already closed the type, we know that ty1 is
           ;; unbound in subst.
           (begin
             ;; since ty2 is guaranteed to be closed, we know there
             ;; can be no occurrence
             ;; (check-no-occurrence! ty1 ty2 exp)
             (extend-subst ty1 ty2 subst)))
          ((tvar-type? ty2)
           (recur ty2 ty1 subst))
          ((and (proc-type? ty1) (proc-type? ty2))
           (cond 
             ((recur
                (proc-type->arg-type ty1)
                (proc-type->arg-type ty2)
                subst)
              =>
              (lambda (subst1)
                (recur
                  (proc-type->result-type ty1)
                  (proc-type->result-type ty2)
                  subst1)))
             (else #f)))
          (else #f)))))

  ;; (trace <:-type)

  (define equiv-type?
    (lambda (ty1 ty2 tenv)
      (equal?
        (expand-type-in-tenv ty1 tenv)
        (expand-type-in-tenv ty2 tenv))))
          
  )